Search Results

Documents authored by Kenison, George

Document
DOI: 10.4230/LIPIcs.STACS.2024.41
Linear Loop Synthesis for Quadratic Invariants

Authors: S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.
Cite as

S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka. Linear Loop Synthesis for Quadratic Invariants. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 41:1-41:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hitarth_et_al:LIPIcs.STACS.2024.41,
  author =	{Hitarth, S. and Kenison, George and Kov\'{a}cs, Laura and Varonka, Anton},
  title =	{{Linear Loop Synthesis for Quadratic Invariants}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{41:1--41:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.41},
  URN =		{urn:nbn:de:0030-drops-197512},
  doi =		{10.4230/LIPIcs.STACS.2024.41},
  annote =	{Keywords: program synthesis, loop invariants, verification, Diophantine equations}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.130
Positivity Problems for Reversible Linear Recurrence Sequences

Authors: George Kenison, Joris Nieuwveld, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
It is a longstanding open problem whether there is an algorithm to decide the Positivity Problem for linear recurrence sequences (LRS) over the integers, namely whether given such a sequence, all its terms are non-negative. Decidability is known for LRS of order 5 or less, i.e., for those sequences in which every new term depends linearly on the previous five (or fewer) terms. For simple LRS (i.e., those sequences whose characteristic polynomials have no repeated roots), decidability of Positivity is known up to order 9. In this paper, we focus on the important subclass of reversible LRS, i.e., those integer LRS ⟨u_n⟩_{n=0}^∞ whose bi-infinite completion ⟨u_n⟩_{n=-∞}^∞ also takes exclusively integer values; a typical example is the classical Fibonacci (bi-)sequence ⟨ … , 5, -3, 2, -1, 1, 0, 1, 1, 2, 3, 5, … ⟩. Our main results are that Positivity is decidable for reversible LRS of order 11 or less, and for simple reversible LRS of order 17 or less.
Cite as

George Kenison, Joris Nieuwveld, Joël Ouaknine, and James Worrell. Positivity Problems for Reversible Linear Recurrence Sequences. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 130:1-130:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kenison_et_al:LIPIcs.ICALP.2023.130,
  author =	{Kenison, George and Nieuwveld, Joris and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{Positivity Problems for Reversible Linear Recurrence Sequences}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{130:1--130:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.130},
  URN =		{urn:nbn:de:0030-drops-181821},
  doi =		{10.4230/LIPIcs.ICALP.2023.130},
  annote =	{Keywords: The Positivity Problem, Linear Recurrence Sequences, Verification}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.61
On the Skolem Problem for Reversible Sequences

Authors: George Kenison

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
Given an integer linear recurrence sequence ⟨X_n⟩, the Skolem Problem asks to determine whether there is a natural number n such that X_n = 0. Recent work by Lipton, Luca, Nieuwveld, Ouaknine, Purser, and Worrell proved that the Skolem Problem is decidable for a class of reversible sequences of order at most seven. Here we give an alternative proof of their result. Our novel approach employs a powerful result for Galois conjugates that lie on two concentric circles due to Dubickas and Smyth.
Cite as

George Kenison. On the Skolem Problem for Reversible Sequences. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 61:1-61:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kenison:LIPIcs.MFCS.2022.61,
  author =	{Kenison, George},
  title =	{{On the Skolem Problem for Reversible Sequences}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{61:1--61:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.61},
  URN =		{urn:nbn:de:0030-drops-168590},
  doi =		{10.4230/LIPIcs.MFCS.2022.61},
  annote =	{Keywords: The Skolem Problem, Linear Recurrences, Verification}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.67
On Positivity and Minimality for Second-Order Holonomic Sequences

Authors: George Kenison, Oleksiy Klurman, Engel Lefaucheux, Florian Luca, Pieter Moree, Joël Ouaknine, Markus A. Whiteland, and James Worrell

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
An infinite sequence ⟨u_n⟩_n of real numbers is holonomic (also known as P-recursive or P-finite) if it satisfies a linear recurrence relation with polynomial coefficients. Such a sequence is said to be positive if each u_n ≥ 0, and minimal if, given any other linearly independent sequence ⟨v_n⟩_n satisfying the same recurrence relation, the ratio u_n/v_n → 0 as n → ∞. In this paper we give a Turing reduction of the problem of deciding positivity of second-order holonomic sequences to that of deciding minimality of such sequences. More specifically, we give a procedure for determining positivity of second-order holonomic sequences that terminates in all but an exceptional number of cases, and we show that in these exceptional cases positivity can be determined using an oracle for deciding minimality.
Cite as

George Kenison, Oleksiy Klurman, Engel Lefaucheux, Florian Luca, Pieter Moree, Joël Ouaknine, Markus A. Whiteland, and James Worrell. On Positivity and Minimality for Second-Order Holonomic Sequences. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 67:1-67:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kenison_et_al:LIPIcs.MFCS.2021.67,
  author =	{Kenison, George and Klurman, Oleksiy and Lefaucheux, Engel and Luca, Florian and Moree, Pieter and Ouaknine, Jo\"{e}l and Whiteland, Markus A. and Worrell, James},
  title =	{{On Positivity and Minimality for Second-Order Holonomic Sequences}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{67:1--67:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.67},
  URN =		{urn:nbn:de:0030-drops-145071},
  doi =		{10.4230/LIPIcs.MFCS.2021.67},
  annote =	{Keywords: Holonomic sequences, Minimal solutions, Positivity Problem}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact